Nuprl Lemma : R-compat-Rlist
0,22
postcript
pdf
L
:Realizer List,
B
:Realizer. (
A
L
.
A
||
B
)
(
L
) ||
B
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
P
Q
,
(
L
)
,
reduce(
f
;
k
;
as
)
,
Y
,
x
.
t
(
x
)
,
x
(
s
)
,
Prop
Lemmas
es
realizer
wf
,
R-compat-none
,
l
all
wf
,
R-compat
wf
origin
L:Realizer List, B:Realizer. (A
L. A || B) 
(L) || B L:Realizer List, B:Realizer. (AL. A || B) (L) || B x:A. B(x) T Q(L)
x. t(x)